<html>
<head><meta charset="utf-8"><title>Mathematical, rigorous safety proofs · t-lang/wg-unsafe-code-guidelines · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/index.html">t-lang/wg-unsafe-code-guidelines</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html">Mathematical, rigorous safety proofs</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="167745190"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167745190" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167745190">(Jun 10 2019 at 09:27)</a>:</h4>
<p>To answer one of your questions <span class="user-mention" data-user-id="211549">@Ehsan M. Kermani</span>:</p>
<blockquote>
<p>Things discussed here are new to me but I'm curious and want to know more. I've been trying to educate myself with UB (what is it exactly?) reading John Regehr's and Ralf's blogs etc. I have to confess that I've got an uneasy feeling that many unanswered questions have deep roots in LLVM itself. I'd like to ask you to what extent we can prove safety? (I mean mathematical, rigorous proofs). I'm aware of miri and Rustbelt, though these're not accessible to me and I don't know the minimum requirements, but what I'm looking at is ideas and intuitions behind validity and safety proofs (if there're some!). Is there any place I can get most of the idea from? (blogs etc.)</p>
</blockquote>
<p>Good question! The fully correct answer is that it is impossible to prove mathematical rigorous things about any compute system. Ultimately these are physical artifacts (hardware and software combined), and physics is outside of what math can prove.<br>
What math can prove things about this is <em>models</em> of physical systems. You start with some assumptions e.g. about how a CPU works, and then you show that <em>if</em> the CPU really works that way, <em>then</em> certain things are true. You can even prove that <em>if</em> the CPU really matches some HDL like Verilog or so, <em>then</em> it works the way we need. But there always is an "if".</p>



<a name="167745356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167745356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167745356">(Jun 10 2019 at 09:30)</a>:</h4>
<p>One of the most rigorously-proven-correct compilers out there is CompCert, but it, too, has assumptions: the parser is not verified (and there were bugs in there, and now they are proving more things about the parser), and you have to trust that CompCert's idea of "what x86 does" is actually correct (and there were bugs there for some architectures that lead to incorrect compilation). So CompCert's proof is more like <em>if</em> the program got parsed correctly and <em>if</em> an x86/ARM/... CPU really works the way this definition says it does and <em>if</em> the output of CompCert (which is textual assembly, no binary) is correctly translated to (binary) machine code and ... <em>then</em> the program will do what it should be doing.<br>
This is still extremely useful though! Not <em>all</em> bugs are excluded, but <em>many</em>, and that is demonstrably useful in <a href="http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf" target="_blank" title="http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf">practical evaluation</a>:</p>
<blockquote>
<p>The striking thing about our CompCert results is that the middle-end bugs we<br>
found in all other compilers are absent. As of early 2011, the<br>
under-development version of CompCert is the only compiler we have tested for<br>
which Csmith cannot find wrong-code errors. This isnot for lack of trying: we<br>
have devoted about six CPU-years to the task. The apparent unbreakability of<br>
CompCert supports a strong argument that developing compiler optimizations<br>
within a proof framework, where safety checks are explicit and<br>
machine-checked, has tangible benefits for compiler users.</p>
</blockquote>



<a name="167745445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167745445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167745445">(Jun 10 2019 at 09:32)</a>:</h4>
<p>so, coming to Rust, we are far from CompCert. ;) What RustBelt shows is that <em>if</em> our model (I am an author of RustBelt) of the borrow checker matches the real borrow checker, and <em>if</em> our model of how MIR programs behave matches what they really do, <em>then</em> we get safety. That's two big IFs, and the are likely both not true!</p>



<a name="167745471"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167745471" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> centril <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167745471">(Jun 10 2019 at 09:33)</a>:</h4>
<p>Personally, I would settle for a soundness proof of Rust's type system according to our TBD chosen operational semantics. <span aria-label="slight smile" class="emoji emoji-1f642" role="img" title="slight smile">:slight_smile:</span></p>



<a name="167745526"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167745526" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167745526">(Jun 10 2019 at 09:34)</a>:</h4>
<p>however, when you bring in LLVM, the question actually to some extend gets worse than just "we have no proof". The problem is that we don't even have a theorem one might want to prove! Before you can prove anything you need a precise statement of what it is you want to prove. In particular we need an operational semantics for what Rust code is actually doing when being executed, and (as @Centril just mentioned) we don't have that currently.</p>



<a name="167745565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167745565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167745565">(Jun 10 2019 at 09:35)</a>:</h4>
<p>And that's where LLVM comes in: defining the operation semantics has the interesting and conflicting set of goals of being a reasonable, understandable semantics on the one hand while at the same time it has to be possible to compile our code to efficient LLVM. But to analyze if that translation is correct, we need <em>both</em> a semantics for Rust/MIR and for LLVM, and currently we have neither...</p>



<a name="167768608"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167768608" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Ehsan M. Kermani <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167768608">(Jun 10 2019 at 15:26)</a>:</h4>
<p>Thank you <span class="user-mention" data-user-id="120791">@RalfJ</span> and <span class="user-mention" data-user-id="126931">@centril</span> for the clarifications! Most of my concerns is about Rust Abstract Machine (given some fundamental assumptions) that right now seems to be far away from being well-defined, yet I cannot get my head around how we can say rustc optimizations are safe and free of UBs!</p>
<p>Can we have an FAQ in the github wg to address what the goals are and what are non-goals? For some time I was under the impression that the goal is to surface what we don't know to future RFC and the ultimate goal is (as Mazdak said) soundness proof of Rust's type system or even coming up with all the necessary definitions for Rust Abstract Machine that future compiler writers, when adhere to, will be provided with all the safety guarantees.</p>



<a name="167770054"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical%2C%20rigorous%20safety%20proofs/near/167770054" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Mathematical.2C.20rigorous.20safety.20proofs.html#167770054">(Jun 10 2019 at 15:44)</a>:</h4>
<p>well defining the Rust Abstract Machine is also a goal</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>